COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		Consider a function \F1term\F0 that that could decide whether
C00003 ENDMK
C⊗;
	Consider a function \F1term\F0 that that could decide whether
the evaluation of an S-expression terminated.  We require that  \F1term e\F0
be \F2true\F0 if \F1eval[e\F0,NIL] terminates and \F2false\F0 otherwise.  For example,
\F1term\F0[(CAR (QUOTE (A B)))] would be \F2true\F0 and \F1term\F0[((LABEL G (LAMBDA (X) (G X)))
(QUOTE A))] would be \F2false\F0.  We assert that no such LISP function term
exists.

	For if \F1term\F0 exists, the there is an S-expression \F1t\F0 that
represents it in S-expression notation.  (E.g. \F1t\F0 might start out
(LABEL TERM (LAMBDA (E) (COND ..etc.).